(declare-sort C)
(declare-const i Int)
(declare-const j Int)
(declare-const e C)
(declare-const a (Array Int C))

(push)

; we assert the premise
(assert (= (select (store a i e) j) e))
; we assert negation of the conclusion
(assert (not (not (= i j))))

; sat means there exists a counterexample!
(check-sat)
;(get-model)

(pop)
(push)

; again we assert the premise
(assert (= (select (store a i e) j) e))
; we assert negation of the conclusion
(assert (not (not (= (select a j) e))))

(check-sat)
;(get-model)

(pop)
(push)

; again we assert the premise
(assert (= (select (store a i e) j) e))
; we assert negation of the conclusion
(assert (not (or (= i j) (= (select a j) e))))

(check-sat)
;(get-model)

(pop)
(push)

(declare-const k Int)
(declare-const f C)
(declare-const g C)

; again we assert the premise(s)
(assert (= (select (store (store a i e) j f) k) g))
(assert (not (= j k)))
(assert (= i j))
; we assert negation of the conclusion
(assert (not (= (select a k) g)))

(check-sat)
;(get-model)